Termination w.r.t. Q of the following Term Rewriting System could be proven:
Q restricted rewrite system:
The TRS R consists of the following rules:
div(X, e) → i(X)
i(div(X, Y)) → div(Y, X)
div(div(X, Y), Z) → div(Y, div(i(X), Z))
Q is empty.
↳ QTRS
↳ DirectTerminationProof
Q restricted rewrite system:
The TRS R consists of the following rules:
div(X, e) → i(X)
i(div(X, Y)) → div(Y, X)
div(div(X, Y), Z) → div(Y, div(i(X), Z))
Q is empty.
We use [23] with the following order to prove termination.
Recursive path order with status [2].
Quasi-Precedence:
[div2, i1]
Status: i1: [1]
div2: [1,2]